import Yices hiding (and, or, not)
import qualified Yices as Y

-- Type synonyms, for readability;
type Time = Nat
type CoordV = Nat
type CoordH = Nat

-- Constants:
nn  = 5 -- size of board
n_s = 24 -- how many stones at the beginning
n_e = 1 -- how many stones at the end
ww = nn -- width of the board
hh = nn -- height of the board
tt  = n_s-n_e -- how many steps to simulate

-- Variables:
ss' :: Ident (Time -> CoordV -> CoordH -> Bool)
(ss',ss) = ident3 "S"

v' :: Ident (Time -> CoordV)
(v',v) = ident1 "v"

h' :: Ident (Time -> CoordH)
(h',h) = ident1 "h"

d' :: Ident (Time -> Bool)
(d',d) = ident1 "d"

s' :: Ident (Time -> Bool)
(s',s) = ident1 "s"

-- Transition between states:
transition :: (Term (CoordV -> CoordH -> Bool), Term CoordV, Term CoordH, Prop, Prop) -> Term (CoordV -> CoordH -> Bool) -> Prop
transition (ss,v,h,d,s) ss' = bounds /\ (ss!v!h) /\ disj (map conj touched) /\ conj untouched
  where
    touched = 
        [ [ h <= nh,     d,     s, ss!v!(h.+1), non (ss!v!(h.+2)), non (ss'!v!h), non (ss'!v!(h.+1)), ss'!v!(h.+2) ]
        , [ h >= 3,      d, non s, ss!v!(h.-1), non (ss!v!(h.-2)), non (ss'!v!h), non (ss'!v!(h.-1)), ss'!v!(h.-2) ]
        , [ v <= nv, non d,     s, ss!(v.+1)!h, non (ss!(v.+2)!h), non (ss'!v!h), non (ss'!(v.+1)!h), ss'!(v.+2)!h ]
        , [ v >= 3,  non d, non s, ss!(v.-1)!h, non (ss!(v.-2)!h), non (ss'!v!h), non (ss'!(v.-1)!h), ss'!(v.-2)!h ]
        ]
    untouched =
        [  ((    d /\     s /\ (v /= i \/ h >= (j+1) \/ h <= (j-3))) ==> (ss ! nat i ! nat j <==> ss' ! nat i ! nat j))
        /\ ((    d /\ non s /\ (v /= i \/ h >= (j+3) \/ h <= (j-1))) ==> (ss ! nat i ! nat j <==> ss' ! nat i ! nat j))
        /\ ((non d /\     s /\ (h /= j \/ v >= (i+1) \/ v <= (i-3))) ==> (ss ! nat i ! nat j <==> ss' ! nat i ! nat j))
        /\ ((non d /\ non s /\ (h /= j \/ v >= (i+3) \/ v <= (i-1))) ==> (ss ! nat i ! nat j <==> ss' ! nat i ! nat j))
        | i <- [1..hh], j <- [1..ww]
        ]
    nh = nn - 2
    nv = nn - 2
    bounds = (h <= nn) /\ (v <= nn) /\ (h >= 1) /\ (v >= 1)
    (.+), (.-) :: Term Nat -> Nat -> Term Nat
    (.+) x y = plus' ! x ! lit y
    (.-) x y = minus' ! x ! lit y
    (<=), (>=), (/=) :: Term Nat -> Nat -> Prop
    (<=) x y = le' ! x ! lit y
    (>=) x y = ge' ! x ! lit y
    (/=) x y = non (eq' ! x ! nat y)

main = generate
    -- Variable definitions
    [ define ss', define v', define h', define d', define s'
    -- Initial position
    , asc [ if (i == 3 && j == 3) then non (ss 0 i j) else ss 0 i j | i <- [1..hh], j <- [1..ww]]
    -- State transitions
    , asc [ transition (ss' ! lit t, v t, h t, d t, s t) (ss' ! lit (t+1)) | t <- [0..tt-1] ]
    ]
  where
    asc = assert . conj
    generate = putStr . unlines . (++["(check)"]) . map show
